A:Type, L:(A List), i:Id, R:({a:A| (a  L)} Realizer).
(R-has-loc(xL.R(x);i))  (xL.R-has-loc(R(x);i)) 

latex

Definitions	False, A, A  B, A c B, x. t(x), , P  Q, P  Q, P & Q, x:A. B(x), (xL.P(x)), x(s), P  Q, (x  l), t  T, x:A. B(x),
Lemmas	l member-set, select wf, length wf1, nat wf, Rall wf, R-has-loc wf, assert wf, list-set-type, assert-Rall-has-loc, Id wf, es realizer wf, l member wf